; benchmark generated from python API
(set-info :status unknown)
(declare-fun basic_right_pic_feasible () Bool)
(declare-fun basic_right_pic_kid_1_feasible () Bool)
(declare-fun basic_right_pic_kid_0_feasible () Bool)
(declare-fun basic_right_pic_kid_0_width () Real)
(declare-fun basic_right_pic_kid_1_width () Real)
(declare-fun basic_right_pic_kid_0_x () Real)
(declare-fun basic_right_pic_kid_1_x () Real)
(declare-fun basic_right_pic_kid_1_y () Real)
(declare-fun basic_right_pic_hight () Real)
(declare-fun basic_right_pic_kid_1_hight () Real)
(declare-fun basic_right_pic_kid_0_hight () Real)
(declare-fun basic_right_pic_kid_0_y () Real)
(declare-fun basic_right_pic_width () Real)
(assert
 (let (($x1254 (not basic_right_pic_feasible)))
 (let (($x2270 (or $x1254 basic_right_pic_kid_1_feasible)))
 (let (($x2268 (not basic_right_pic_kid_1_feasible)))
 (let (($x2269 (or $x2268 basic_right_pic_feasible)))
 (let (($x2267 (or $x1254 basic_right_pic_kid_0_feasible)))
 (let (($x2265 (not basic_right_pic_kid_0_feasible)))
 (let (($x2266 (or $x2265 basic_right_pic_feasible)))
 (let (($x2263 (= (+ (- basic_right_pic_kid_1_width) basic_right_pic_kid_0_width) 0.0)))
 (let (($x2264 (or $x1254 $x2263)))
 (let ((?x2238 (- (- basic_right_pic_kid_1_x basic_right_pic_kid_0_x) basic_right_pic_kid_0_width)))
 (let (($x2260 (or $x1254 (= ?x2238 0.0))))
 (let ((?x2256 (+ (- basic_right_pic_kid_1_hight basic_right_pic_hight) basic_right_pic_kid_1_y)))
 (let (($x2258 (or $x1254 (= ?x2256 0.0))))
 (let ((?x2252 (- (+ basic_right_pic_kid_0_y basic_right_pic_kid_0_hight) basic_right_pic_hight)))
 (let (($x2254 (or $x1254 (= ?x2252 0.0))))
 (let (($x2250 (or $x1254 (= basic_right_pic_kid_1_y 0.0))))
 (let (($x2248 (or $x1254 (= basic_right_pic_kid_0_y 0.0))))
 (let ((?x2244 (- (+ basic_right_pic_kid_1_x basic_right_pic_kid_1_width) basic_right_pic_width)))
 (let (($x2246 (or $x1254 (= ?x2244 0.0))))
 (let (($x2242 (or $x1254 (= basic_right_pic_kid_0_x 0.0))))
 (let (($x2240 (or $x1254 (>= ?x2238 0.0))))
 (let ((?x2234 (- (+ (- basic_right_pic_kid_1_hight) basic_right_pic_hight) basic_right_pic_kid_1_y)))
 (let (($x2236 (or $x1254 (>= ?x2234 0.0))))
 (let (($x2210 (>= basic_right_pic_kid_1_y 0.0)))
 (let (($x2231 (or $x1254 $x2210)))
 (let ((?x2228 (+ (- (- basic_right_pic_kid_1_x) basic_right_pic_kid_1_width) basic_right_pic_width)))
 (let (($x2230 (or $x1254 (>= ?x2228 0.0))))
 (let (($x2209 (>= basic_right_pic_kid_1_x 0.0)))
 (let (($x2225 (or $x1254 $x2209)))
 (let ((?x2222 (+ (- (- basic_right_pic_kid_0_y) basic_right_pic_kid_0_hight) basic_right_pic_hight)))
 (let (($x2224 (or $x1254 (>= ?x2222 0.0))))
 (let (($x2206 (>= basic_right_pic_kid_0_y 0.0)))
 (let (($x2219 (or $x1254 $x2206)))
 (let ((?x2216 (+ (- (- basic_right_pic_kid_0_x) basic_right_pic_kid_0_width) basic_right_pic_width)))
 (let (($x2218 (or $x1254 (>= ?x2216 0.0))))
 (let (($x2205 (>= basic_right_pic_kid_0_x 0.0)))
 (let (($x2213 (or $x1254 $x2205)))
 (let (($x2212 (>= basic_right_pic_kid_1_hight 0.0)))
 (let (($x2211 (>= basic_right_pic_kid_1_width 0.0)))
 (let (($x2208 (>= basic_right_pic_kid_0_hight 0.0)))
 (let (($x2207 (>= basic_right_pic_kid_0_width 0.0)))
 (and $x2205 $x2206 $x2207 $x2208 $x2209 $x2210 $x2211 $x2212 $x2213 $x2218 $x2219 $x2224 $x2225 $x2230 $x2231 $x2236 $x2240 $x2242 $x2246 $x2248 $x2250 $x2254 $x2258 $x2260 $x2264 $x2266 $x2267 $x2269 $x2270 basic_right_pic_feasible)))))))))))))))))))))))))))))))))))))))))))
(check-sat)

